deferred type t : *
deferred val e : t

let h [y] (f, x) where (y = e and pre (f) (x))
returns z where (y = e)
=
 0

let g (x) where (x = 0) = x

let x = h [e] (g, 0)
  
